es:ES, e:E. x:E. (x loc e  & (first(x))) 

latex

Definitions	P  Q, A c B, e loc e' , P  Q, x:A. B(x), P & Q, x:A. B(x), , t  T, Dec(P)
Lemmas	es-le weakening, es-locl transitivity1, es-pred-locl, es-loc-pred, es-pred-causl, es-pred wf, es-locl wf, es-le weakening eq, decidable assert, event system wf, es-causl wf, es-first wf, assert wf, es-le wf, es-E wf